0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 0 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 10 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 0 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 PiDP
↳9 UsableRulesProof (⇔, 0 ms)
↳10 PiDP
↳11 PiDPToQDPProof (⇒, 7 ms)
↳12 QDP
↳13 QDPSizeChangeProof (⇔, 0 ms)
↳14 YES
flB_in_gga([], [], 0) → flB_out_gga([], [], 0)
flB_in_gga(.(T8, T9), T10, s(T12)) → U3_gga(T8, T9, T10, T12, pA_in_gagga(T8, X13, T10, T9, T12))
pA_in_gagga([], T17, T17, T9, T12) → U1_gagga(T17, T9, T12, flB_in_gga(T9, T17, T12))
U1_gagga(T17, T9, T12, flB_out_gga(T9, T17, T12)) → pA_out_gagga([], T17, T17, T9, T12)
pA_in_gagga(.(T24, T25), X38, .(T24, T26), T9, T12) → U2_gagga(T24, T25, X38, T26, T9, T12, pA_in_gagga(T25, X38, T26, T9, T12))
U2_gagga(T24, T25, X38, T26, T9, T12, pA_out_gagga(T25, X38, T26, T9, T12)) → pA_out_gagga(.(T24, T25), X38, .(T24, T26), T9, T12)
U3_gga(T8, T9, T10, T12, pA_out_gagga(T8, X13, T10, T9, T12)) → flB_out_gga(.(T8, T9), T10, s(T12))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
flB_in_gga([], [], 0) → flB_out_gga([], [], 0)
flB_in_gga(.(T8, T9), T10, s(T12)) → U3_gga(T8, T9, T10, T12, pA_in_gagga(T8, X13, T10, T9, T12))
pA_in_gagga([], T17, T17, T9, T12) → U1_gagga(T17, T9, T12, flB_in_gga(T9, T17, T12))
U1_gagga(T17, T9, T12, flB_out_gga(T9, T17, T12)) → pA_out_gagga([], T17, T17, T9, T12)
pA_in_gagga(.(T24, T25), X38, .(T24, T26), T9, T12) → U2_gagga(T24, T25, X38, T26, T9, T12, pA_in_gagga(T25, X38, T26, T9, T12))
U2_gagga(T24, T25, X38, T26, T9, T12, pA_out_gagga(T25, X38, T26, T9, T12)) → pA_out_gagga(.(T24, T25), X38, .(T24, T26), T9, T12)
U3_gga(T8, T9, T10, T12, pA_out_gagga(T8, X13, T10, T9, T12)) → flB_out_gga(.(T8, T9), T10, s(T12))
FLB_IN_GGA(.(T8, T9), T10, s(T12)) → U3_GGA(T8, T9, T10, T12, pA_in_gagga(T8, X13, T10, T9, T12))
FLB_IN_GGA(.(T8, T9), T10, s(T12)) → PA_IN_GAGGA(T8, X13, T10, T9, T12)
PA_IN_GAGGA([], T17, T17, T9, T12) → U1_GAGGA(T17, T9, T12, flB_in_gga(T9, T17, T12))
PA_IN_GAGGA([], T17, T17, T9, T12) → FLB_IN_GGA(T9, T17, T12)
PA_IN_GAGGA(.(T24, T25), X38, .(T24, T26), T9, T12) → U2_GAGGA(T24, T25, X38, T26, T9, T12, pA_in_gagga(T25, X38, T26, T9, T12))
PA_IN_GAGGA(.(T24, T25), X38, .(T24, T26), T9, T12) → PA_IN_GAGGA(T25, X38, T26, T9, T12)
flB_in_gga([], [], 0) → flB_out_gga([], [], 0)
flB_in_gga(.(T8, T9), T10, s(T12)) → U3_gga(T8, T9, T10, T12, pA_in_gagga(T8, X13, T10, T9, T12))
pA_in_gagga([], T17, T17, T9, T12) → U1_gagga(T17, T9, T12, flB_in_gga(T9, T17, T12))
U1_gagga(T17, T9, T12, flB_out_gga(T9, T17, T12)) → pA_out_gagga([], T17, T17, T9, T12)
pA_in_gagga(.(T24, T25), X38, .(T24, T26), T9, T12) → U2_gagga(T24, T25, X38, T26, T9, T12, pA_in_gagga(T25, X38, T26, T9, T12))
U2_gagga(T24, T25, X38, T26, T9, T12, pA_out_gagga(T25, X38, T26, T9, T12)) → pA_out_gagga(.(T24, T25), X38, .(T24, T26), T9, T12)
U3_gga(T8, T9, T10, T12, pA_out_gagga(T8, X13, T10, T9, T12)) → flB_out_gga(.(T8, T9), T10, s(T12))
FLB_IN_GGA(.(T8, T9), T10, s(T12)) → U3_GGA(T8, T9, T10, T12, pA_in_gagga(T8, X13, T10, T9, T12))
FLB_IN_GGA(.(T8, T9), T10, s(T12)) → PA_IN_GAGGA(T8, X13, T10, T9, T12)
PA_IN_GAGGA([], T17, T17, T9, T12) → U1_GAGGA(T17, T9, T12, flB_in_gga(T9, T17, T12))
PA_IN_GAGGA([], T17, T17, T9, T12) → FLB_IN_GGA(T9, T17, T12)
PA_IN_GAGGA(.(T24, T25), X38, .(T24, T26), T9, T12) → U2_GAGGA(T24, T25, X38, T26, T9, T12, pA_in_gagga(T25, X38, T26, T9, T12))
PA_IN_GAGGA(.(T24, T25), X38, .(T24, T26), T9, T12) → PA_IN_GAGGA(T25, X38, T26, T9, T12)
flB_in_gga([], [], 0) → flB_out_gga([], [], 0)
flB_in_gga(.(T8, T9), T10, s(T12)) → U3_gga(T8, T9, T10, T12, pA_in_gagga(T8, X13, T10, T9, T12))
pA_in_gagga([], T17, T17, T9, T12) → U1_gagga(T17, T9, T12, flB_in_gga(T9, T17, T12))
U1_gagga(T17, T9, T12, flB_out_gga(T9, T17, T12)) → pA_out_gagga([], T17, T17, T9, T12)
pA_in_gagga(.(T24, T25), X38, .(T24, T26), T9, T12) → U2_gagga(T24, T25, X38, T26, T9, T12, pA_in_gagga(T25, X38, T26, T9, T12))
U2_gagga(T24, T25, X38, T26, T9, T12, pA_out_gagga(T25, X38, T26, T9, T12)) → pA_out_gagga(.(T24, T25), X38, .(T24, T26), T9, T12)
U3_gga(T8, T9, T10, T12, pA_out_gagga(T8, X13, T10, T9, T12)) → flB_out_gga(.(T8, T9), T10, s(T12))
FLB_IN_GGA(.(T8, T9), T10, s(T12)) → PA_IN_GAGGA(T8, X13, T10, T9, T12)
PA_IN_GAGGA([], T17, T17, T9, T12) → FLB_IN_GGA(T9, T17, T12)
PA_IN_GAGGA(.(T24, T25), X38, .(T24, T26), T9, T12) → PA_IN_GAGGA(T25, X38, T26, T9, T12)
flB_in_gga([], [], 0) → flB_out_gga([], [], 0)
flB_in_gga(.(T8, T9), T10, s(T12)) → U3_gga(T8, T9, T10, T12, pA_in_gagga(T8, X13, T10, T9, T12))
pA_in_gagga([], T17, T17, T9, T12) → U1_gagga(T17, T9, T12, flB_in_gga(T9, T17, T12))
U1_gagga(T17, T9, T12, flB_out_gga(T9, T17, T12)) → pA_out_gagga([], T17, T17, T9, T12)
pA_in_gagga(.(T24, T25), X38, .(T24, T26), T9, T12) → U2_gagga(T24, T25, X38, T26, T9, T12, pA_in_gagga(T25, X38, T26, T9, T12))
U2_gagga(T24, T25, X38, T26, T9, T12, pA_out_gagga(T25, X38, T26, T9, T12)) → pA_out_gagga(.(T24, T25), X38, .(T24, T26), T9, T12)
U3_gga(T8, T9, T10, T12, pA_out_gagga(T8, X13, T10, T9, T12)) → flB_out_gga(.(T8, T9), T10, s(T12))
FLB_IN_GGA(.(T8, T9), T10, s(T12)) → PA_IN_GAGGA(T8, X13, T10, T9, T12)
PA_IN_GAGGA([], T17, T17, T9, T12) → FLB_IN_GGA(T9, T17, T12)
PA_IN_GAGGA(.(T24, T25), X38, .(T24, T26), T9, T12) → PA_IN_GAGGA(T25, X38, T26, T9, T12)
FLB_IN_GGA(.(T8, T9), T10) → PA_IN_GAGGA(T8, T10, T9)
PA_IN_GAGGA([], T17, T9) → FLB_IN_GGA(T9, T17)
PA_IN_GAGGA(.(T24, T25), .(T24, T26), T9) → PA_IN_GAGGA(T25, T26, T9)
From the DPs we obtained the following set of size-change graphs: